One or more embodiments disclosed within this specification relate to security analysis of computer programs.
Static program analysis enables complex properties of a program to be provided via over-approximation of the program's runtime behavior, which reduces the state space required for a proof. A real-world example of static program analysis in the field of security analysis is downgrader detection. A downgrader can be implemented as a sanitizer and/or as a validator used in security analysis. A sanitizer performs transformation on program code, while a validator typically merely performs validation.
When security analysis is performed, information flows sometimes are seeded by statements in the program that read as user inputs, which are known as sources. These statements are tracked. If there is a path from a source to a security-sensitive operation, known as a sink, which does not go through either sanitization or validation by a downgrader, then a vulnerability is reported.